Topological vector spaces #1300
Conversation
mkerjean
added
the
TODO: MC2 port
|
For the record, a previous comment on PR#539, now closed by @zstone1 "With a long-term goal of doing spectral theory, I'm looking at defining integrals for a TVS. The most straightforward choice seems to be "weak integrals"." |
affeldt-aist
added
experiment 🧪
|
The last commit makes the dev compile but it is clearly a temporary fix. |
mkerjean
force-pushed
the
evt2
branch
4 times, most recently
from
d8a9777 to
3388bf1
Compare
mkerjean
force-pushed
the
evt2
branch
2 times, most recently
from
a53018d to
a6da51e
Compare
mkerjean
added
enhancement ✨
mkerjean
force-pushed
the
evt2
branch
2 times, most recently
from
68c3907 to
185a571
Compare
There was a problem hiding this comment.
Mostly looks great. A few renamings, a few nitpicks. And I know you're already on top of the duplication with resepct to normedtype.v.
The only one I think is blocking is removing the "lawless joins" between Filtered/nbhs/topological + modules. I wouldn't care so much if structures could be declared locally. But globally adding these structures seems like something we'll regret later. If approach doesn't work, let me know and we can figure out something else.
theories/tvs.v
Outdated
| Local Open Scope classical_set_scope. | ||
| Local Open Scope ring_scope. | ||
|
|
||
| HB.structure Definition PointedNmodule := {M of Pointed M & GRing.Nmodule M}. |
There was a problem hiding this comment.
Nitpicks: since HB has rather strong requirements that
- you can't define joins twice
- you must define joins "bottom-up" in the hierarchy
It's a bit more forward-compatible to define in the earliest places they can. The Pointed + something from mathcomp can live next to pointed.
There was a problem hiding this comment.
Thanks for the suggestion, I'll make the change and resolve the conversation when done.
theories/tvs.v
Outdated
| Local Open Scope ring_scope. | ||
|
|
||
| HB.structure Definition PointedNmodule := {M of Pointed M & GRing.Nmodule M}. | ||
| HB.structure Definition PointedZmodule := {M of Pointed M & GRing.Zmodule M}. |
There was a problem hiding this comment.
Note: In topology.v we have
HB.instance Definition _ (R : zmodType) := isPointed.Build R 0.
which conflicts with this structure. I'm not sure if it will matter in practice, and honestly I'm not even sure why we have that instance in topology.v at all. If we could safely remove that from topology that would be great. Mostly this is a heads up that this structure has bad inheritance paths.
theories/tvs.v
Outdated
| HB.structure Definition PointedLmodule (K : numDomainType) := {M of Pointed M & GRing.Lmodule K M}. | ||
|
|
||
| HB.structure Definition FilteredNmodule := {M of Filtered M M & GRing.Nmodule M}. | ||
| HB.structure Definition FilteredZmodule := {M of Filtered M M & GRing.Zmodule M}. |
There was a problem hiding this comment.
To resolve before merge: Having these joins without the natural compatibility mixins (AKA continuity) concerns me a bit. Since these things have a uniform structure anyway, doing it with the TopologicalLmod_isTvs factory makes a lot sense. But I also see that you use nbhs0N_subproof twice, and these structures are useful for refactoring that.
I think there is an alternative that get best of both worlds. I'm not sure if this is the "right way" to do it, but a viable approach is to take the group structure as an extra argument:
Section properties_of_topologicallmodule.
Context (R : numDomainType) (E : topologicalType)
(Me : GRing.Lmodule R E) (U : set E).
Let ME := GRing.Lmodule.Pack Me.
Lemma nbhsN_subproof (f : continuous (fun z : R^o * E => z.1 *: (z.2 : ME))) (x : E) :
nbhs x U -> nbhs (-(x:ME)) (-%R @` (U : set ME)).
Proof.
move => Ux; move: (@f (-1,-(x:ME)) U); rewrite /= scaleN1r opprK => /(_ Ux) [] /=.
move => [B] B12 [B1 B2] BU; near=> y; exists (-(y:ME)); rewrite ?opprK -?scaleN1r //.
apply: (BU (-1,y)); split => /=; last by near:y; rewrite nearE.
by move: B1 => [] //= ? ?; apply => [] /=; rewrite subrr normr0.
Unshelve. all: by end_near. Qed.
Then when E has a lmodule structure, you use GRing.Lmodule.class E to extract it. So you have to add a few extra annotations, but this quirk is hidden inside these subproof lemmas. I haven't tried this all the way, so I can't confirm yet that it will actually 100%, but I'm optimisitc
There was a problem hiding this comment.
Adding your solution within the section properties_of_topologicallmodule, with a few 0 : E to be specified in the factory TopologicalLmod_isTvs , in the sense that the Pointed/Filtered + N/z/Lmodules instances can be deleted. The following joins, involving Nbhs, Topological and Uniform, are still necessary. Is this still an issue? Is there a way to define these joins locally?
There was a problem hiding this comment.
I'm a little confused why they are necessary? The file does build (on my machine) without those joins. Is there a result you have in mind that relies one of the lawless joins? If they are necessary then that's fine, but if they can be removed that would be better.
There was a problem hiding this comment.
On my machine normedtype.v does not build when the modification is done to tvs.v, as there is an issue for the definition of PseudoMetricNormedZmod (l. 255). Taking out the Uniform + Lmodule join gives the following error message:
You must declare the hierarchy bottom-up or addd a missing join.
There are two ways out:
- declare structure PseudoMetricNormedZmod before structure Tvs if Tvs inherits from it;
- declare an additional structure that inherits from both Uniform and GRing.Zmodule and from which PseudoMetricNormedZmod and/or Tvs inherit.
I have to say it's unclear to me why taking out the pointed and filtered joins does not create an issue like this one.
There was a problem hiding this comment.
Ah! I see what's happening here. You're right, it does seem hopeless to remove these. Sorry for sending you down a rabbit hole!
There was a problem hiding this comment.
Context (R : numDomainType) (E : topologicalType) (Me : GRing.Lmodule R E) (U : set E). Let ME := GRing.Lmodule.Pack Me.
@zstone1 @mkerjean @Tragicus This proof does not work since coq/coq#19611 because GRing.Lmodule.sort ME no longer triggers canonical structure inference and gets reduced immediately. Can't we just use the TopologicalLmodule structure instead?
There was a problem hiding this comment.
Yeah, it's fine with me. If we have to have topologicalLmodule anyway, we might as well use it.
There was a problem hiding this comment.
There are a few comments in this PR that point at code duplication; just after it is merged, I think it would be good to open an issue with links to duplications so that they can be taken care of later.
I think that I already asked, but in the section prod_NormedModule, numDomainType gets specialized to numFieldType: is it unavoidable? (I remember that I double-checked myself and got to the conclusion that it is but I do not remember precisely.)
The commented HB.structure at the top of the type tvs.v can maybe be deleted.
@CohenCyril, do you see anything potentially problematic?
|
Rebasing the branch over mc-analysis 1.6.0, and in particular over the PR splitting topology in multiple files, makes the compilation fail. |
I am not sure but that maybe because you have some |
|
I encountered a possibly similar issue where a stray |
|
In such cases, I tend to use |
Co-authored with Reynald Affeldt <[email protected]> Co-authored with Cyril Cohen <[email protected]> Co-authored with Zachary Stone @zstone1
|
\o/ |
Motivation for this change
Adding topological vector spaces as a new structure. Further PRs will integrate the theory of topological vector spaces (duality, function spaces, characterization of topologies, distribution theory)
Checklist
CHANGELOG_UNRELEASED.mdReference: How to document
Reminder to reviewers